Theorem 3expia 1121

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 456	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  ad5ant125  1368  mp3an3  1452  3gencl  3484  vtocl3gaf  3536  vtocl3ga  3538  moi  3676  disji  5083  disjord  5087  3optocl  5721  sossfld  6144  f1oresrab  7072  f1cdmsn  7228  soisores  7273  isomin  7283  isofrlem  7286  ovmpos  7506  ov2gf  7507  ndmovord  7548  nnsuc  7826  poxp  8070  frpoins3xp3g  8083  brtpos  8177  dfsmo2  8279  smoiun  8293  smoord  8297  smogt  8299  omeulem1  8509  omeu  8512  oewordi  8519  uniinqs  8734  mapvalg  8773  pmvalg  8774  elmapg  8776  xpdom3  9003  mapdom3  9077  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  php3  9133  nndomog  9137  onomeneq  9138  sucdom  9144  unxpdomlem3  9158  isinf  9165  f1finf1o  9173  isfinite2  9198  prfi  9224  ordiso  9421  cnfcom3clem  9614  r111  9687  tskwe  9862  pr2ne  9915  infxpenlem  9923  dfac8alem  9939  infdif  10118  infdif2  10119  cff1  10168  coflim  10171  cfslbn  10177  cfslb2n  10178  cofsmo  10179  cfsmolem  10180  cfcoflem  10182  fin23lem27  10238  isf32lem9  10271  isf34lem6  10290  axcc2lem  10346  domtriomlem  10352  axdc4lem  10365  zorn2lem2  10407  axdclem2  10430  konigthlem  10479  gchen1  10536  gchen2  10537  gchpwdom  10581  gchaleph  10582  winainflem  10604  tskcard  10692  gruiun  10710  gruen  10723  intgru  10725  grudomon  10728  grur1a  10730  grutsk1  10732  nqereu  10840  nqereq  10846  ltsonq  10880  prlem934  10944  reclem3pr  10960  1re  11132  axsup  11208  addlid  11316  recex  11769  lemul1a  11995  lt2msq  12027  fimaxre2  12087  zdiv  12562  zextlt  12566  prime  12573  uzind2  12585  fzind  12590  lbzbi  12849  qbtwnxr  13115  qextltlem  13117  xralrple  13120  xltneg  13132  xlt2add  13175  supxrgtmnf  13244  ixxub  13282  ixxlb  13283  ioo0  13286  ico0  13307  ioc0  13308  icc0  13309  iocssre  13343  icossre  13344  iccssre  13345  fzen  13457  expclzlem  14006  expaddz  14029  expmulz  14031  hashgadd  14300  hashunsngx  14316  hashgt23el  14347  elovmpowrd  14481  pfxnd0  14612  ccatopth2  14640  pfxccatin12  14656  cshf1  14733  shftuz  14992  cau3lem  15278  caubnd  15282  climuni  15475  lo1resb  15487  o1resb  15489  o1of2  15536  o1add  15537  o1mul  15538  o1sub  15539  ntrivcvgmul  15825  eflt  16042  moddvds  16190  dvdscmulr  16211  dvdsmulcr  16212  dvdsle  16237  divalglem8  16327  divalgb  16331  ndvdssub  16336  bitsfzo  16362  gcdcllem1  16426  gcdcllem3  16428  dvdsgcd  16471  nn0rppwr  16488  nn0expgcd  16491  lcmgcdlem  16533  lcmfeq0b  16557  qredeu  16585  isprm3  16610  prmdvdsexpr  16644  prmexpb  16646  eulerthlem2  16709  fermltl  16711  coprimeprodsq  16736  pythagtrip  16762  pcprendvds  16768  pcpremul  16771  pcdvdsb  16797  pc2dvds  16807  4sqlem12  16884  4sqlem18  16890  vdwlem10  16918  cshwshashlem3  17025  xpsrnbas  17492  ismred  17521  mrieqv2d  17562  iscatd  17596  isfuncd  17789  fthestrcsetc  18073  fthsetcestrc  18088  poslubd  18334  dirtr  18525  mulgaddcom  19028  ghmrn  19158  pmtrprfv3  19383  mndodcongi  19472  oddvdsnn0  19473  oddvds  19476  odcl2  19494  odhash3  19505  gexdvds  19513  pgpfi  19534  lsmss1b  19595  lsmss2b  19597  efgsrel  19663  efgred  19677  cntzcmn  19769  cyggenod  19813  lt6abl  19824  gsumcom2  19904  pgpfac1lem2  20006  pgpfac1lem3  20008  dvdsunit  20315  unitmulclb  20317  irredrmul  20363  isabvd  20745  lmodvsdi  20836  lss0cl  20898  islbs3  21110  lbsextlem2  21114  xrsdsreclblem  21367  psrbaglefi  21882  mvrf1  21941  coe1fzgsumd  22248  gsummoncoe1  22252  evl1gsumd  22301  scmataddcl  22460  scmatsubcl  22461  mdetunilem9  22564  mdetuni0  22565  mdetmul  22567  m2cpmrngiso  22702  pm2mpf1  22743  opnnei  23064  neindisj2  23067  cncls2  23217  cncls  23218  cnntr  23219  cnpresti  23232  cnprest  23233  lmcnp  23248  isreg2  23321  ordthauslem  23327  unconn  23373  2ndc1stc  23395  kgen2ss  23499  ptclsg  23559  cnmptcom  23622  kqfvima  23674  hmeof1o  23708  fbncp  23783  fbfinnfr  23785  trfbas2  23787  isufil2  23852  ufprim  23853  trufil  23854  filufint  23864  hausflim  23925  flimrest  23927  flimcls  23929  cnpfcf  23985  alexsubALT  23995  tmdgsum  24039  opnsubg  24052  cldsubg  24055  qustgpopn  24064  tsmsxp  24099  blpnf  24341  blssps  24368  blss  24369  blssec  24379  neibl  24445  prdsxmslem2  24473  xrsmopn  24757  metnrm  24807  climcncf  24849  iccpnfhmeo  24899  xrhmeo  24900  bndth  24913  cphsqrtcl3  25143  iscau2  25233  iscmet3lem2  25248  bcthlem5  25284  bcth3  25287  ishl2  25326  ivthlem1  25408  cmmbl  25491  iundisj2  25506  voliunlem2  25508  mbfaddlem  25617  itg2itg1  25693  itg2seq  25699  itg2mulclem  25703  cnplimc  25844  dvres2  25869  deg1nn0clb  26051  deg1lt0  26052  deg1ge  26059  plypf1  26173  plyadd  26178  plymul  26179  coeeu  26186  dgrub2  26196  coeidlem  26198  coeid3  26201  coemullem  26211  coe11  26214  coemulhi  26215  coemulc  26216  dgreq0  26227  dgrlt  26228  dgradd2  26230  vieta1lem2  26275  tanord1  26502  tanord  26503  logccne0  26543  cxpeq0  26643  cxpmul2z  26656  cxpcn3lem  26713  rtprmirr  26726  relogbzcl  26740  angpieqvd  26797  o1cxp  26941  scvxcvx  26952  chtublem  27178  bposlem3  27253  lgsqr  27318  2sqnn  27406  dchrisumlema  27455  dchrisumlem2  27457  ostth2lem3  27602  nosepon  27633  noextenddif  27636  nolesgn2o  27639  nogesgn1o  27641  nosepne  27648  nodense  27660  onnolt  28262  onlts  28263  oniso  28267  bdayn0p1  28365  bdayn0sf1o  28366  tghilberti2  28710  inagswap  28913  f1otrg  28943  brbtwn2  28978  axpasch  29014  axcontlem4  29040  axcontlem5  29041  upgredg2vtx  29214  usgredg2vtxeuALT  29295  sizusglecusg  29537  upgredginwlk  29709  frgrwopreg1  30393  frgrwopreg2  30394  frgrregorufrg  30401  lpni  30555  ipasslem5  30910  htthlem  30992  omlsii  31478  spansni  31632  spansneleq  31645  elspansn4  31648  sumspansn  31724  homco1  31876  homulass  31877  mdsl0  32385  ssdmd1  32388  ssdmd2  32389  cvdmd  32412  chirredlem2  32466  atdmd  32473  atmd2  32475  disjif  32653  iundisj2f  32665  isoun  32781  preiman0  32789  padct  32797  iocinioc2  32859  iundisj2fi  32877  sgn3da  32915  sgnnbi  32919  sgnpbi  32920  indpi1  32941  archiabllem1a  33273  archiabllem2a  33276  slmdvsdi  33297  ordtconnlem1  34081  measinblem  34377  measres  34379  measdivcstALTV  34382  mbfmco2  34422  orvclteinc  34633  bnj605  35063  bnj607  35072  bnj964  35099  bnj1033  35125  bnj1128  35146  bnj1137  35151  bnj1136  35153  bnj1413  35191  bnj60  35218  rankfilimb  35258  r1filim  35260  fineqvac  35272  fineqvnttrclselem3  35279  fineqvnttrclse  35280  cusgredgex  35316  subgrwlk  35326  acycgr1v  35343  cvmlift2lem10  35506  msubvrs  35754  wsuclem  36017  dfrdg4  36145  brcolinear2  36252  brsegle2  36303  nn0prpw  36517  ntruni  36521  clsint2  36523  fnessref  36551  fnemeet2  36561  fnejoin2  36563  limsucncmpi  36639  ee7.2aOLD  36655  bj-idreseq  37367  dissneqlem  37545  isbasisrelowllem1  37560  isbasisrelowllem2  37561  icoreclin  37562  poimirlem9  37830  poimirlem30  37851  poimirlem32  37853  areacirc  37914  filbcmb  37941  mettrifi  37958  heiborlem8  38019  heiborlem10  38021  heibor  38022  riscer  38189  igenval2  38267  lshpcmp  39248  eqlkr  39359  lkrlsp2  39363  lkrshp  39365  cvrnbtwn2  39535  cvlexch3  39592  cvlexch4N  39593  cvlatexchb1  39594  cvlsupr3  39604  exatleN  39664  cvratlem  39681  atcvrj2b  39692  cvrat3  39702  cvrat4  39703  athgt  39716  ps-1  39737  ps-2  39738  3atlem5  39747  3at  39750  llnneat  39774  llnmlplnN  39799  lplnneat  39805  lplnnelln  39806  islpln2a  39808  lplnriaN  39810  lplnribN  39811  lplnexllnN  39824  2llnjaN  39826  lvolnle3at  39842  lvolneatN  39848  lvolnelln  39849  lvolnelpln  39850  islvol2aN  39852  dalem62  39994  pmapglb2N  40031  pmapglb2xN  40032  lncmp  40043  paddasslem14  40093  paddasslem15  40094  pmod2iN  40109  hlmod1i  40116  pclfinclN  40210  osumcllem8N  40223  pexmidlem4N  40233  pl42lem1N  40239  pl42lem4N  40242  lhpexle1  40268  lhpexle2lem  40269  lhpmcvr5N  40287  lhpmcvr6N  40288  ltrneq  40409  trlnidatb  40437  cdleme0ex2N  40484  cdleme27a  40627  cdleme17d3  40756  cdlemeg46gfre  40792  cdleme48gfv1  40796  cdlemeg49lebilem  40799  cdlemf2  40822  cdlemf  40823  cdlemfnid  40824  trlord  40829  cdlemg31c  40959  cdlemg35  40973  trlcone  40988  tendoeq2  41034  cdlemj3  41083  cdlemk26b-3  41165  cdlemk33N  41169  cdleml3N  41238  cdlemn  41472  dih1dimb2  41501  dihord5apre  41522  dihmeetlem1N  41550  dihglblem5apreN  41551  dihglblem2N  41554  dihglblem3N  41555  dihmeetlem13N  41579  dihmeetlem15N  41581  dihatexv  41598  hdmap14lem12  42139  uzindd  42231  lcmineqlem1  42283  sticksstones1  42400  dvdsexpnn0  42589  frlmfzowrdb  42759  oddcomabszz  43186  jm2.19lem4  43234  fiuneneq  43434  idomsubgmo  43435  omcl2  43575  pwinfi3  43804  gneispa  44371  mnringmulrcld  44469  grumnudlem  44526  ismnushort  44542  binomcxplemnn0  44590  addrcom  44715  int3  44853  suctrALT  45066  suctrALTcf  45162  suctrALT3  45164  chordthmALT  45173  iunconnlem2  45175  relpmin  45193  relpfrlem  45194  stoweidlem26  46270  stoweidlem34  46278  issald  46577  goldbachth  47793  grlimgrtri  48249  nnsgrp  48423  ply1mulgsumlem1  48632  lubsscl  49205  glbsscl  49206