Theorem jcad 522

Description: Deduction conjoining the consequents of two implications. Deduction form of jca 521 and double deduction form of pm3.2 475 and pm3.2i 476. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses

Ref	Expression
jcad.1	⊢ (𝜑 → (𝜓 → 𝜒))
jcad.2	⊢ (𝜑 → (𝜓 → 𝜃))

Assertion

Ref	Expression
jcad	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jcad

Step	Hyp	Ref	Expression
1		jcad.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jcad.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		pm3.2 475	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 71	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  jca2  523  jctild  535  jctird  536  ancld  560  ancrd  561  oplem1  1072  2eu1  2678  2eu1v  2679  disjxiun  5103  iss  6039  oneqmini  6434  funssres  6604  elpreimaOLD  7081  isomin  7368  oneqmin  7838  frxp  8165  soseq  8203  tposfo2  8294  oa00  8595  odi  8615  oneo  8617  oeordsuc  8631  oelim2  8632  nnarcl  8653  nnmord  8669  nnneo  8692  map0g  8940  pssnn  9212  fodomfib  9348  inf3lem4  9659  cplem1  9977  cplem1OLD  9978  kardenOLD  9987  setrec1lem4  9998  alephordi  10180  cardinfima  10203  dfac5lem5  10233  isf34lem4  10482  axcc4  10544  axdc3lem2  10556  zorn2lem4  10604  zorn2lem7  10607  indpi  11019  genpcl  11120  addclprlem2  11129  ltaddpr  11146  ltexprlem5  11152  suplem1pr  11164  ltlen  11438  dedekind  11500  sup2  12300  nominpos  12610  uzind  12818  xrmaxlt  13338  xrltmin  13339  xrmaxle  13340  xrlemin  13341  xmullem2  13422  ccatopth  14893  shftuz  15251  sqreulem  15556  limsupbnd2  15679  mulcn2  15792  sadcaddlem  16656  dvdsgcdb  16747  algcvgblem  16781  lcmdvdsb  16817  rpexp  16927  infpnlem1  17117  divsfval  17748  iscatd  17876  posasymb  18522  plttr  18543  joinle  18587  meetle  18601  latnlej  18659  latnlej2  18662  lsmlub  19908  imasring  20590  unitmulclb  20641  lbspss  21387  lspsneu  21431  lspprat  21461  assapropd  22209  isclo2  23436  cncls2  23621  cncls  23622  cnntr  23623  cnrest2  23634  cmpsub  23748  cmpcld  23750  kgenss  23892  ptpjpre1  23920  txlm  23997  qtoptop2  24048  cmphaushmeo  24149  fbun  24189  isfild  24207  fbasrn  24233  fgtr  24239  ufinffr  24278  rnelfm  24302  fmfnfmlem4  24306  ghmcnp  24464  metrest  24873  icoopnst  25290  iocopnst  25291  dvfsumlem2  26377  dgreq0  26614  plyexmo  26666  taylthlem2  26731  cxpeq0  27036  mumullem2  27537  chpchtsum  27576  bposlem7  27647  lgsqr  27708  ltsres  28049  nosupno  28090  noinfno  28105  ltlesnd  28162  uspgr2wlkeq  30256  subgrwlk  30299  wwlknllvtx  30465  ex-natded5.3-2  31039  ubthlem1  31502  axhcompl-zf  31630  ococss  31925  nmopun  32646  elpjrn  32822  stm1addi  32877  stm1add3i  32879  mdsl1i  32953  chrelat2i  32997  atexch  33013  atcvat4i  33029  mdsymlem3  33037  bnj600  35619  trssfihf  35819  trssfihfregs  35904  karddom  35929  kardsdom  35930  pthacycspth  36079  srepdflem1  36085  subfacval2  36119  climuzcnv  36603  3jcadALT  36619  fundmpss  36710  segconeq  36953  ifscgr  36987  endofsegid  37028  colinbtwnle  37061  trer  37282  ivthALT  37301  fnessref  37323  fnemeet2  37333  fnejoin2  37335  onsuct0  37407  bj-ideqg1  38277  bj-elid6  38283  bj-finsumval0  38398  bj-isrvec2  38413  bj-bary1  38425  icorempo  38466  isbasisrelowllem1  38470  isbasisrelowllem2  38471  relowlpssretop  38479  finxpsuclem  38512  poimirlem31  38761  isbnd2  38909  bfplem2  38949  ghomco  39017  cnf1dd  39214  contrd  39221  mpobi123f  39286  mptbi12f  39290  iss2  39468  refressn  39657  jca2r  40104  prter2  40130  lshpset2N  40368  cvrnbtwn2  40524  cvrnbtwn3  40525  cvrnbtwn4  40528  cvlcvr1  40588  hlrelat2  40652  cvrat4  40692  islpln2a  40797  linepsubN  41001  elpaddn0  41049  paddssw2  41093  pmapjoin  41101  ispsubcl2N  41196  dochkrshp  42635  dochsatshp  42700  mapdh9a  43038  hdmap11lem2  43091  sn-sup2  43748  frlmfzowrdb  43764  pwinfi3  44756  clsk1independent  45238  gneispace  45326  pm11.71  45573  relpmin  46137  ormkglobd  48092  2reu8i  48389  sbgoldbaltlem2  49083  oppcendc  50337