Theorem 3jca 821

Description: Join consequents with conjunction.

Hypotheses

Ref	Expression
3jca.1	⊢ (φ → ψ)
3jca.2	⊢ (φ → χ)
3jca.3	⊢ (φ → θ)

Assertion

Ref	Expression
3jca	⊢ (φ → (ψ ⋀ χ ⋀ θ))

Proof of Theorem 3jca

Step	Hyp	Ref	Expression
1		3jca.1	. . . 4 ⊢ (φ → ψ)
2		3jca.2	. . . 4 ⊢ (φ → χ)
3	1, 2	jca 288	. . 3 ⊢ (φ → (ψ ⋀ χ))
4		3jca.3	. . 3 ⊢ (φ → θ)
5	3, 4	jca 288	. 2 ⊢ (φ → ((ψ ⋀ χ) ⋀ θ))
6		df-3an 779	. 2 ⊢ ((ψ ⋀ χ ⋀ θ) ↔ ((ψ ⋀ χ) ⋀ θ))
7	5, 6	sylibr 200	1 ⊢ (φ → (ψ ⋀ χ ⋀ θ))

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 777

This theorem is referenced by:  3jcad 822  syl3anc 860  tpss 2480  ordelord 2976  limuni3 3129  tz7.49 3965  alephval3 4914  ltexpq 5092  le2tri3 5601  divdivdivt 5787  divdiv23t 5794  divdivmult 5797  ltmul12it 5843  ltdivmultOLD 5870  ledivmultOLD 5871  lt2mul2divt 5874  lediv2t 5893  ltdiv23t 5894  lediv23t 5895  ledivp1t 5907  flval3t 6241  flhalft 6248  quoremz 6253  intfrac 6254  intfracq 6255  elioo4g 6386  iccsupr 6399  lbicc2t 6405  ubicc2t 6406  uztrn 6429  eluzp1p1t 6436  peano2uz 6448  eluzfz1t 6488  elfzuzt 6489  eluzfz2t 6490  elfz2nn0t 6496  fznn0sub2t 6500  elfzp1 6511  fzrev3t 6515  fseqsupub 6527  expsubt 6599  expordit 6601  expubndt 6609  bernneq 6653  expnbndt 6655  absdivz 6859  seq1ublem 6911  facdivt 6942  facndivt 6943  faclbnd 6945  faclbnd3 6947  bcnp11t 6965  permnnt 6973  fsumcmp0 7041  serzcmp0 7055  climaddc1 7118  climmullem4 7123  climsub 7130  climsubc2 7131  climcmpc1 7139  iserzcmp 7142  caucvg3a 7164  caucvg3lem 7166  iserzabslem 7178  expcnv 7233  georeclim 7240  geoisum1c 7245  cvgratlem2 7251  efaddlem5 7342  efaddlem10 7347  efaddlem16 7353  efaddlem19 7356  efaddlem23 7360  efaddlem26 7363  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  eirrlem2 7390  eflegeolem1 7413  eflegeolem2 7414  efcnlem1 7419  reeff1o 7426  sin02gt0 7479  acdc3lem 7487  acdc2lem2 7490  acdc5lem2 7493  infxp 7573  clsndisj 7703  cnco 7765  cnpco 7766  blss 7850  ssblex 7853  methausi 7878  metcnpf 7880  metcnplem 7883  tgioolem 7911  lmuni 7948  lmle 7957  bopcnlem2 7979  iscms2lem4 7989  cmsss 7994  bcthlem8 8003  bcthlem9 8004  bcthlem18 8013  grpidinvlem2 8046  grpidinvlem4 8048  grpinvid1 8068  grpinvid2 8069  grplcan 8071  grp2inv 8074  grpinvf 8075  grpinvop 8076  grpmuldivass 8084  grppncan 8086  grpnpcan 8087  grppnpcan2 8088  grpnpncan 8090  abl4 8101  abldivdiv4 8105  ablnnncan 8107  ablnnncan1 8109  cnring 8158  ringsn 8159  vc0 8184  vcm 8186  vcoprne 8194  isnvi 8228  nvmdi 8266  nvmul0or 8268  nvsubadd 8271  nvpncan2 8272  nvnpcan 8276  nvnncan 8279  nvmeq0 8280  nvdif 8289  nvabs 8297  nvelbl 8321  nvcnpf 8324  nvlmle 8329  sqcn 8331  nmcn3 8337  nmcnc 8338  sm1cnilem 8343  sspg 8383  ssps 8385  lno0 8413  lnomul 8417  nvcnpi3 8418  nvcnpi4 8419  nmoub3i 8432  nmblore 8442  nmblolbii 8455  blocni 8461  ipasslem4 8489  ubthlem12 8536  minveclem30 8570  htthlem10 8625  psasym 8647  pstr 8648  pilem1 8666  efif1lem1 8725  efif1lem2 8726  osumlem3 9575  elunop2t 9933  nmbdoplb 9944  nmcopexlem3 9948  nmcopexlem5 9950  nmcoplb 9953  nmophm 9956  lnopcon 9958  nmbdfnlb 9973  nmcfnexlem3 9977  nmcfnexlem5 9979  nmcfnlb 9982  lnfncon 9985  riesz3 9990  cnlnadjlem2 9996  cnlnadjlem7 10001  nmopadjlem 10017  nmopco 10023  leopnmidt 10066  nmopleidt 10067  hmopidmchlem 10073  pjclem4 10122  pj3s 10130  stle 10162  hstrlem3a 10182  csmdsym 10256  superpos 10276  atexcht 10303  atcvatlem 10307  atcvat4 10319  cdj3 10363  inposet 10477  cdrci 10480  truni1 10485  cmphmp 10507  idhme 10508  cnvhmpha 10511  cnvhmphb 10512  hmphre 10516  hmpher 10522  hmeogrp 10524  eqindhome 10527  hmeobc 10528  oefil2 10552  neifil 10553  filintf 10554  fgsb 10555  fgsb2 10560  rcfpfil 10569  dtt2 10589  mslb1 10600  iintlem1 10603  iint 10605  trnij 10608  homgrf 10701  imonclem 10712  ismonc 10713  idmon 10716  immon 10717  idfisf 10731

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779

Copyright terms: Public domain