Theorem 3expia 1139

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 1138	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 462	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

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

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

This theorem is used by:  ad5ant125OLD  1391  mp3an3  1479  3gencl  3493  vtocl3gaf  3539  vtocl3ga  3540  moi  3675  disji  5087  disjord  5091  3optocl  5748  sossfld  6179  f1oresrab  7131  f1cdmsn  7292  soisores  7337  isomin  7347  isofrlem  7350  ovmpos  7570  ov2gf  7571  ndmovord  7613  nnsuc  7897  poxp  8144  frpoins3xp3g  8162  brtpos  8257  dfsmo2  8360  smoiun  8374  smoord  8378  smogt  8380  omeulem1  8595  omeu  8598  oewordi  8605  uniinqs  8823  mapvalg  8861  pmvalg  8862  elmapg  8864  xpdom3  9099  mapdom3  9173  sdomdomtrfi  9221  domsdomtrfi  9222  php  9227  php3  9229  nndomog  9233  onomeneq  9234  sucdom  9240  unxpdomlem3  9254  isinf  9261  f1finf1o  9269  isfinite2  9295  prfi  9320  ordiso  9515  cnfcom3clem  9711  r111  9787  tskwe  10036  pr2ne  10089  infxpenlem  10097  dfac8alem  10113  infdif  10291  infdif2  10292  cff1  10341  coflim  10344  cfslbn  10350  cfslb2n  10351  cofsmo  10352  cfsmolem  10353  cfcoflem  10355  fin23lem27  10411  isf32lem9  10444  isf34lem6  10463  axcc2lem  10519  domtriomlem  10525  axdc4lem  10538  zorn2lem2  10580  axdclem2  10603  konigthlem  10658  gchen1  10715  gchen2  10716  gchpwdom  10760  gchaleph  10761  winainflem  10783  tskcard  10871  gruiun  10889  gruen  10902  intgru  10904  grudomon  10907  grur1a  10909  grutsk1  10911  nqereu  11019  nqereq  11025  ltsonq  11059  prlem934  11123  reclem3pr  11139  1re  11313  axsup  11390  addlid  11498  recex  11953  lemul1a  12176  lt2msq  12207  fimaxre2  12267  indpi1  12339  zdiv  12774  zextlt  12778  prime  12785  uzind2  12797  fzind  12802  lbzbi  13068  qbtwnxr  13335  qextltlem  13337  xralrple  13340  xltneg  13352  xlt2add  13395  supxrgtmnf  13464  ixxub  13502  ixxlb  13503  ioo0  13506  ico0  13527  ioc0  13528  icc0  13529  iocssre  13563  icossre  13564  iccssre  13565  fzen  13679  expclzlem  14231  expaddz  14254  expmulz  14256  hashgadd  14526  hashunsngx  14542  hashgt23el  14574  elovmpowrd  14708  pfxnd0  14844  ccatopth2  14872  pfxccatin12  14888  cshf1  14967  shftuz  15229  sgn3da  15261  sgnnbi  15264  sgnpbi  15265  cau3lem  15529  caubnd  15533  climuni  15726  lo1resb  15738  o1resb  15740  o1of2  15787  o1add  15788  o1mul  15789  o1sub  15790  ntrivcvgmul  16078  eflt  16292  moddvds  16440  dvdscmulr  16461  dvdsmulcr  16462  dvdsle  16487  divalglem8  16577  divalgb  16581  ndvdssub  16586  bitsfzo  16612  gcdcllem1  16676  gcdcllem3  16678  dvdsgcd  16724  nn0rppwr  16742  nn0expgcd  16745  lcmgcdlem  16788  lcmfeq0b  16812  qredeu  16840  isprm3  16865  prmdvdsexpr  16900  prmexpb  16902  eulerthlem2  16966  fermltl  16968  coprimeprodsq  16993  pythagtrip  17019  pcprendvds  17025  pcpremul  17028  pcdvdsb  17054  pc2dvds  17064  4sqlem12  17141  4sqlem18  17147  vdwlem10  17175  cshwshashlem3  17282  xpsrnbas  17750  ismred  17779  mrieqv2d  17820  iscatd  17854  isfuncd  18047  fthestrcsetc  18331  fthsetcestrc  18346  poslubd  18592  dirtr  18783  mulgaddcom  19315  ghmrn  19450  pmtrprfv3  19675  mndodcongi  19764  oddvdsnn0  19765  oddvds  19768  odcl2  19786  odhash3  19797  gexdvds  19805  pgpfi  19826  lsmss1b  19887  lsmss2b  19889  efgsrel  19955  efgred  19969  cntzcmn  20061  cyggenod  20105  lt6abl  20116  gsumcom2  20196  pgpfac1lem2  20298  pgpfac1lem3  20300  dvdsunit  20616  unitmulclb  20618  irredrmul  20664  isabvd  21076  lmodvsdi  21167  lss0cl  21229  islbs3  21440  lbsextlem2  21444  rspprop  21531  xrsdsreclblem  21726  psrbaglefi  22241  mvrf1  22300  coe1fzgsumd  22629  gsummoncoe1  22633  evl1gsumd  22682  scmataddcl  22838  scmatsubcl  22839  mdetunilem9  22942  mdetuni0  22943  mdetmul  22945  m2cpmrngiso  23083  pm2mpf1  23124  opnnei  23445  neindisj2  23448  cncls2  23598  cncls  23599  cnntr  23600  cnpresti  23613  cnprest  23614  lmcnp  23629  isreg2  23702  ordthauslem  23708  unconn  23754  2ndc1stc  23776  kgen2ss  23881  ptclsg  23941  cnmptcom  24004  kqfvima  24056  hmeof1o  24090  fbncp  24165  fbfinnfr  24167  trfbas2  24169  isufil2  24234  ufprim  24235  trufil  24236  filufint  24246  hausflim  24307  flimrest  24309  flimcls  24311  cnpfcf  24367  alexsubALT  24377  tmdgsum  24421  opnsubg  24434  cldsubg  24437  qustgpopn  24446  tsmsxp  24481  blpnf  24723  blssps  24750  blss  24751  blssec  24761  neibl  24827  prdsxmslem2  24855  xrsmopn  25139  metnrm  25189  climcncf  25228  iccpnfhmeo  25273  xrhmeo  25274  bndth  25286  cphsqrtcl3  25515  iscau2  25605  iscmet3lem2  25620  bcthlem5  25656  bcth3  25659  ishl2  25698  ivthlem1  25779  cmmbl  25862  iundisj2  25877  voliunlem2  25879  mbfaddlem  25988  itg2itg1  26064  itg2seq  26070  itg2mulclem  26074  cnplimc  26214  dvres2  26239  deg1nn0clb  26415  deg1lt0  26416  deg1ge  26423  plypf1  26538  plyadd  26543  plymul  26544  coeeu  26551  dgrub2  26561  coeidlem  26563  coeid3  26566  coemullem  26576  coe11  26579  coemulhi  26580  coemulc  26581  dgreq0  26591  dgrlt  26592  dgradd2  26594  vieta1lem2  26641  tanord1  26872  tanord  26873  logccne0  26913  cxpeq0  27013  cxpmul2z  27026  cxpcn3lem  27082  rtprmirr  27095  relogbzcl  27109  angpieqvd  27166  o1cxp  27309  scvxcvx  27320  chtublem  27545  bposlem3  27620  lgsqr  27685  2sqnn  27773  dchrisumlema  27822  dchrisumlem2  27824  ostth2lem3  27969  nosepon  28029  noextenddif  28032  nolesgn2o  28035  nogesgn1o  28037  nosepne  28044  nodense  28056  onnolt  28659  onlts  28660  oniso  28664  bdayn0p1  28762  bdayn0sf1o  28763  tghilberti2  29113  inagswap  29367  f1otrg  29455  brbtwn2  29490  axpasch  29526  axcontlem4  29552  axcontlem5  29553  upgredg2vtx  29726  usgredg2vtxeuALT  29810  sizusglecusg  30051  upgredginwlk  30223  subgrwlk  30276  frgrwopreg1  30926  frgrwopreg2  30927  frgrregorufrg  30934  lpni  31089  ipasslem5  31444  htthlem  31526  omlsii  32012  spansni  32166  spansneleq  32179  elspansn4  32182  sumspansn  32258  homco1  32410  homulass  32411  mdsl0  32919  ssdmd1  32922  ssdmd2  32923  cvdmd  32946  chirredlem2  33000  atdmd  33007  atmd2  33009  disjif  33221  iundisj2f  33233  acunirnmpt2f  33304  isoun  33344  preiman0  33352  padct  33359  iocinioc2  33419  iundisj2fi  33437  archiabllem1a  33800  archiabllem2a  33803  slmdvsdi  33824  ordtconnlem1  34604  measinblem  34901  measres  34903  measdivcstALTV  34906  mbfmco2  34945  orvclteinc  35156  bnj605  35585  bnj607  35594  bnj964  35621  bnj1033  35647  bnj1128  35668  bnj1137  35673  bnj1136  35675  bnj1413  35713  bnj60  35740  soinfdom  35770  rankfilimb  35782  r1filim  35783  nelscottrankgt  35805  weexenwe  35814  acwer1prc  35818  fineqvac  35842  fineqvnttrclselem3  35849  fineqvnttrclse  35850  j0ltaleph  35949  onprcf1acwevdlem1  35966  onprcf1acwevd  35968  vonf1oonfo  35970  cusgredgex  35984  acycgr1v  35992  cvmlift2lem10  36165  msubvrs  36413  wsuclem  36681  dfrdg4  36809  brcolinear2  36917  brsegle2  36968  nn0prpw  37205  ntruni  37209  clsint2  37211  fnessref  37239  fnemeet2  37249  fnejoin2  37251  limsucncmpi  37327  ee7.2aOLD  37343  bj-idreseq  38190  dissneqlem  38370  isbasisrelowllem1  38385  isbasisrelowllem2  38386  icoreclin  38387  poimirlem9  38654  poimirlem30  38675  poimirlem32  38677  areacirc  38738  filbcmb  38781  mettrifi  38798  heiborlem8  38859  heiborlem10  38861  heibor  38862  riscer  39029  igenval2  39107  eldisjim3  39854  eldisjs6  39979  lshpcmp  40152  eqlkr  40263  lkrlsp2  40267  lkrshp  40269  cvrnbtwn2  40439  cvlexch3  40496  cvlexch4N  40497  cvlatexchb1  40498  cvlsupr3  40508  exatleN  40568  cvratlem  40585  atcvrj2b  40596  cvrat3  40606  cvrat4  40607  athgt  40620  ps-1  40641  ps-2  40642  3atlem5  40651  3at  40654  llnneat  40678  llnmlplnN  40703  lplnneat  40709  lplnnelln  40710  islpln2a  40712  lplnriaN  40714  lplnribN  40715  lplnexllnN  40728  2llnjaN  40730  lvolnle3at  40746  lvolneatN  40752  lvolnelln  40753  lvolnelpln  40754  islvol2aN  40756  dalem62  40898  pmapglb2N  40935  pmapglb2xN  40936  lncmp  40947  paddasslem14  40997  paddasslem15  40998  pmod2iN  41013  hlmod1i  41020  pclfinclN  41114  osumcllem8N  41127  pexmidlem4N  41137  pl42lem1N  41143  pl42lem4N  41146  lhpexle1  41172  lhpexle2lem  41173  lhpmcvr5N  41191  lhpmcvr6N  41192  ltrneq  41313  trlnidatb  41341  cdleme0ex2N  41388  cdleme27a  41531  cdleme17d3  41660  cdlemeg46gfre  41696  cdleme48gfv1  41700  cdlemeg49lebilem  41703  cdlemf2  41726  cdlemf  41727  cdlemfnid  41728  trlord  41733  cdlemg31c  41863  cdlemg35  41877  trlcone  41892  tendoeq2  41938  cdlemj3  41987  cdlemk26b-3  42069  cdlemk33N  42073  cdleml3N  42142  cdlemn  42376  dih1dimb2  42405  dihord5apre  42426  dihmeetlem1N  42454  dihglblem5apreN  42455  dihglblem2N  42458  dihglblem3N  42459  dihmeetlem13N  42483  dihmeetlem15N  42485  dihatexv  42502  hdmap14lem12  43043  uzindd  43135  lcmineqlem1  43186  sticksstones1  43303  dvdsexpnn0  43493  frlmfzowrdb  43678  oddcomabszz  44058  jm2.19lem4  44106  fiuneneq  44301  idomsubgmo  44302  omcl2  44442  pwinfi3  44671  gneispa  45237  mnringmulrcld  45333  grumnudlem  45376  ismnushort  45392  binomcxplemnn0  45440  addrcom  45564  int3  45702  suctrALT  45915  suctrALTcf  46011  suctrALT3  46013  chordthmALT  46022  iunconnlem2  46024  relpmin  46049  relpfrlem  46050  stoweidlem26  47143  stoweidlem34  47151  issald  47450  goldbachth  48739  nprmdvdsfacm1  48816  grlimgrtri  49208  nnsgrp  49381  ply1mulgsumlem1  49605  lubsscl  50181  glbsscl  50182