Theorem jcad 512

Description: Deduction conjoining the consequents of two implications. Deduction form of jca 511 and double deduction form of pm3.2 469 and pm3.2i 470. (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 469	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 70	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  jca2  513  jctild  525  jctird  526  ancld  550  ancrd  551  oplem1  1056  2eu1  2646  2eu1v  2647  disjxiun  5088  iss  5984  oneqmini  6359  funssres  6525  elpreima  6991  isomin  7271  oneqmin  7733  frxp  8056  soseq  8089  tposfo2  8179  oa00  8474  odi  8494  oneo  8496  oeordsuc  8509  oelim2  8510  nnarcl  8531  nnmord  8547  nnneo  8570  map0g  8808  pssnn  9078  fodomfib  9213  fodomfibOLD  9215  inf3lem4  9521  cplem1  9779  karden  9785  alephordi  9962  cardinfima  9985  dfac5lem5  10015  isf34lem4  10265  axcc4  10327  axdc3lem2  10339  zorn2lem4  10387  zorn2lem7  10390  indpi  10795  genpcl  10896  addclprlem2  10905  ltaddpr  10922  ltexprlem5  10928  suplem1pr  10940  ltlen  11211  dedekind  11273  mulgt1OLD  11977  sup2  12075  nominpos  12355  uzind  12562  xrmaxlt  13077  xrltmin  13078  xrmaxle  13079  xrlemin  13080  xmullem2  13161  ccatopth  14620  shftuz  14973  sqreulem  15264  limsupbnd2  15387  mulcn2  15500  sadcaddlem  16365  dvdsgcdb  16453  algcvgblem  16485  lcmdvdsb  16521  rpexp  16630  infpnlem1  16819  divsfval  17448  iscatd  17576  posasymb  18222  plttr  18243  joinle  18287  meetle  18301  latnlej  18359  latnlej2  18362  lsmlub  19574  imasring  20246  unitmulclb  20297  lbspss  21014  lspsneu  21058  lspprat  21088  assapropd  21807  isclo2  23001  cncls2  23186  cncls  23187  cnntr  23188  cnrest2  23199  cmpsub  23313  cmpcld  23315  kgenss  23456  ptpjpre1  23484  txlm  23561  qtoptop2  23612  cmphaushmeo  23713  fbun  23753  isfild  23771  fbasrn  23797  fgtr  23803  ufinffr  23842  rnelfm  23866  fmfnfmlem4  23870  ghmcnp  24028  metrest  24437  icoopnst  24861  iocopnst  24862  dvfsumlem2  25958  dgreq0  26196  plyexmo  26246  taylthlem2  26307  cxpeq0  26612  mumullem2  27115  chpchtsum  27155  bposlem7  27226  lgsqr  27287  sltres  27599  nosupno  27640  noinfno  27655  sltlend  27708  uspgr2wlkeq  29622  wwlknllvtx  29822  ex-natded5.3-2  30383  ubthlem1  30845  axhcompl-zf  30973  ococss  31268  nmopun  31989  elpjrn  32165  stm1addi  32220  stm1add3i  32222  mdsl1i  32296  chrelat2i  32340  atexch  32356  atcvat4i  32372  mdsymlem3  32380  bian1dOLD  32431  bnj600  34926  trssfir1omregs  35120  subgrwlk  35164  pthacycspth  35189  subfacval2  35219  climuzcnv  35703  3jcadALT  35719  fundmpss  35799  segconeq  36043  ifscgr  36077  endofsegid  36118  colinbtwnle  36151  trer  36349  ivthALT  36368  fnessref  36390  fnemeet2  36400  fnejoin2  36402  onsuct0  36474  bj-ideqg1  37197  bj-elid6  37203  bj-finsumval0  37318  bj-isrvec2  37333  bj-bary1  37345  icorempo  37384  isbasisrelowllem1  37388  isbasisrelowllem2  37389  relowlpssretop  37397  finxpsuclem  37430  pibt2  37450  poimirlem31  37690  isbnd2  37822  bfplem2  37862  ghomco  37930  cnf1dd  38129  contrd  38136  mpobi123f  38201  mptbi12f  38205  iss2  38371  refressn  38479  jca2r  38893  prter2  38919  lshpset2N  39157  cvrnbtwn2  39313  cvrnbtwn3  39314  cvrnbtwn4  39317  cvlcvr1  39377  hlrelat2  39441  cvrat4  39481  islpln2a  39586  linepsubN  39790  elpaddn0  39838  paddssw2  39882  pmapjoin  39890  ispsubcl2N  39985  dochkrshp  41424  dochsatshp  41489  mapdh9a  41827  hdmap11lem2  41880  sn-sup2  42523  frlmfzowrdb  42536  pwinfi3  43595  clsk1independent  44078  gneispace  44166  pm11.71  44429  relpmin  44984  ormkglobd  46912  2reu8i  47143  sbgoldbaltlem2  47810  oppcendc  49049  setrec1lem4  49721